$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $a$:ecl(${\it ds}$;${\it da}$), $n$:$\mathbb{N}$. eclthrow($a$;$n$) $\in$ ecl(${\it ds}$;${\it da}$)